COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<to raproachment???>>
C00017 ENDMK
C⊗;
.<<to raproachment???>>
.P283:
We have seen a related result  in the problem on {yon(P271)},
where we were to show that %3fact#=#%7t%3[fact]%1.
That is, %3fact%1 is a solution to the equation %7t%3[x]#=#x%1.
Solutions  to such equations are called %2⊗→fixed points↔←%1.
.GROUP;
The %3fact%1 result is an instance of a more general result:

.BEGIN TABIT1(20);

\for any %7t%1,  define %3h <= λ[[g] %7t%3[function[λ[[x] g[g[x]]]]]%1
(%DY%1)
\then %3h[function[h]]#=#%7t%3[h[function[h]]]%1.
.END
.APART

We shall not prove this result but 
we can give some insight into  its justification
as we develop the mathematical properties of
%3label%1; we continue our discussion of {yonss(P85)}.
Recall %7D%4e%1 and %7D%4a%1 from {yon(P283)}.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%41%*,#...,#t%4n%*)#=#%dg(t%41%*,#...,#t%4n%*)%1.
So:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
We must be a bit careful.
Our treatment of non-local
variables in LISP (on {yon(P93)} and in {yonss(P77)}) requires that these
variables  be evaluated when the function is %2activated%*
rather than when
 the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its non-local variables.
So its denotation 
should be a mapping like: %denv%*#→#%d[%aS%8n%d#→#%aS%d]%1 rather than
simply %d[%aS%8n%d#→#%aS%d]%1. This is consistent with our understanding of the
meaning of λ-notation.
It is what %3function%* was attempting to 
describe. 
What we previously have called an ⊗→open function↔← is  of the
form: %d[%aS%8n%d#→#%aS%d]%1.
Given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*.
.END


A modification of our handling of %3label%* is required to describe the case 
for recursion:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.
Since this interpretation of %3label%* is inadequate in
general contexts,
we should  look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. Recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; %et%3 → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation and will return  a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it imposes the minimal structure on the function⊗↓Like 
a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. This discussion of "least" brings in the recent work of D. Scott
and  the intuition behind
this study  again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).

.GROUP;
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; %et%3 → +[f[n-1];*[2;sub1[n]]]]]
.END
.APART;

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When or if, we realize that the LISP function 
denotes   the "squaring function" for non-negative integers,
then we have moved from pragmatics to semantics.
 The process of discovering
the denotation  may be likened to  a limiting process which
converges to a function satisfying the LISP definition. 
.GROUP;
That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n) n%82%d)%1 = %1limit of the %d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =
\ %9B%1 if %di%c<%dn%1 or %dn%1%c<%d0%1

.END
.APART

We may think of our "equation-solver" as proceeding in such a manner.
As with simpler equations, there may be several solutions. For example,
we have seen that a function, %3g%1, defined to be %3n!%1 for %3n%a≥%30%1 and
%30%1 for %3n%a<%30%1 also satisfies the LISP definition of %3fact%1.
The expected solution for %3fact%1 is undefined for %3n%a<%30%1, and is
therefore  "less defined" than %3g%1. We would like our equation solver
to produce a minimal solution, if possible.


.GROUP;
That is, %dY%1 applied to a term %7t%1 gives a function %df%1 satisfying
%df#=#%7t%d(f)%1.
.BEGIN CENTER;

%dY(%7t%d) = %7t%d(Y(%7t%d))%1
.END
Also %df%1 is minimal is the sense that any other  function
which satisfies the equation is more defined than %df%1. Compare this with
{yon(P283)}. The result there says for any %7t%1

.BEGIN CENTER;
%dY(%7t%d) = h(h)%1### where### %dh(g) = %7t%d( %9λ%d((x) g(g(x))))%1.

.END
.APART;
Such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%*. It is 
designated here by %dY%*. To comprehend %dY%1 we generalize from the previous 
example.

.GROUP;
In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) if(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n) n%82%d) %1for %dn %c≥%d0%1 is the desired solution.
.APART

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %9B%*#⊗↓This
%9B%1 is the totally undefined function in %d[%aFn%d#→#%aFn%d]%1.←.


.GROUP;
.BEGIN CENTER;
%9t%d(%9B%d) = %9λ%d((n) if(n=0, 0, %9B%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%9B%*)%1 is just %df%41%1.
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%9B%*))#=#%9λ%d((n) if(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Writing %9t%8i%1 for the composition of %9t%1...%9t%1, i times, ⊗↓Define
%9t%80%1 to be  %9B%1 in %d[%aFn%d→%aFn%d]%1.← we can say
.BEGIN CENTER;GROUP;

%df%4i%* = %9t%8i%d(%9B%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4i → ∞%9t%8i%d(%9B%d)%1.
.END
.APART

.GROUP;
It can be shown that
the least fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4i→∞%9t%8n%d(%9B%d).%1
.END
.END 
.APART

.GROUP;

So the denotation for %3label%* might be better described by:

.BEGIN CENTERIT;FILL;TURN ON "#";

←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%f(%ag%f)%d(l%1#:#%d<f,h>))%1.
.END

rather than:
.BEGIN CENTERIT;FILL;TURN ON "#";

←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END
.APART


The characterizations are not equivalent. The
behavior of %9D%4a%f(%3label[car;car]%f)%1 will exhibit a discrepancy.
The fix-point characterization reduces %3label[car;car]%1 to the minimal
solution of the equation %dcar#=car%1; that solution is %9B%1.
The LISP interpretation of %3label[car;car]%1 gives %dcar%1.
The general question of the correctness of the denotational semantics which we
are developing is the subject of ⊗↑[Gor#73]↑.